/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import java.lang.annotation.Annotation;
import java.util.Collection;
import java.util.List;
import java.util.logging.Level;
import java.util.logging.Logger;

import org.eclipse.core.resources.IMarker;
import org.eclipse.core.resources.IResource;
import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.jdt.core.ICompilationUnit;
import org.eclipse.jdt.core.IJavaElement;
import org.eclipse.jdt.core.ISourceReference;
import org.eclipse.jdt.core.ITypeRoot;
import org.eclipse.jdt.core.JavaModelException;
import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.CompilationUnit;
import org.eclipse.jdt.core.dom.ConstructorInvocation;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.IMethodBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.SuperConstructorInvocation;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclaration;

import com.googlecode.syper.anno.BoundsChecks;
import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;
import com.googlecode.syper.anno.NullChecks;
import com.googlecode.syper.anno.ReturnExcl;
import com.googlecode.syper.anno.ReturnImm;
import com.googlecode.syper.javasyp.checker.ExpressionEncoder.Lookup;
import com.googlecode.syper.javasyp.formulae.Formula;

import edu.cmu.cs.crystal.IAnalysisInput;
import edu.cmu.cs.crystal.IAnalysisReporter;
import edu.cmu.cs.crystal.ICrystalAnalysis;
import edu.cmu.cs.crystal.annotations.AnnotationSummary;
import edu.cmu.cs.crystal.annotations.ICrystalAnnotation;
import edu.cmu.cs.crystal.internal.Crystal;
import edu.cmu.cs.crystal.util.Option;

/**
 * @author kevin
 *
 */
public class SymbolicChecker implements ICrystalAnalysis, IChecker {

	private static final Logger logger = Logger.getLogger(SymbolicChecker.class.getName());

	/** Started fresh on every analysis run... */
	private ContractRegistry reg;

	private IAnalysisInput input;

	private IAnalysisReporter reporter;

	@Override
	public void afterAllCompilationUnits() {
		reg = null; // allow GC to clean up
	}

	@Override
	public void beforeAllCompilationUnits() {
		try {
			// check whether JML-enabled AST nodes are in the classpath
			Class.forName("org.eclipse.jdt.core.dom.SpecMethodDeclaration", false,
					Thread.currentThread().getContextClassLoader());
			reg = new JmlContractRegistry();
			logger.info("JML support available");
			return;
		} catch (ClassNotFoundException e) {
			logger.log(Level.FINE, "JML support not available", e);
		}
		if (reg == null)
			reg = new ContractRegistry();
	}

	/**
	 * Backwards-compatibility to Crystal 3.4
	 * @param reporter
	 * @param input
	 * @param compUnit
	 * @param rootNode
	 * @see #runAnalysis(IAnalysisReporter, IAnalysisInput, ITypeRoot, CompilationUnit)
	 */
	public void runAnalysis(IAnalysisReporter reporter, IAnalysisInput input,
			ICompilationUnit compUnit, CompilationUnit rootNode) {
		runAnalysis(reporter, input, compUnit, rootNode);
	}

	public void runAnalysis(IAnalysisReporter reporter, IAnalysisInput input,
			ITypeRoot compUnit, CompilationUnit rootNode) {
		this.input = input;
		this.reporter = reporter;
		reg.setAnnos(getInput().getAnnoDB());
		SymbolicMethodVisitor v = createVisitor();
		v.setChecker(this);
		long start = System.currentTimeMillis();
		rootNode.accept(v);
		long millis = System.currentTimeMillis() - start;
		logger.info(String.format("%s checked in %,.3f s with SMT solver taking %,.3f s",
				compUnit.getElementName(),
				millis / 1000.0,
				v.getSolverMillis() / 1000.0));
	}

	@Override
	public IAnalysisInput getInput() {
		return input;
	}

	@Override
	public String getName() {
		return "SymbolicChecker";
	}

	@Override
	public IAnalysisReporter getReporter() {
		return reporter;
	}

	private SymbolicMethodVisitor createVisitor() {
		return new HeapMapLogicMethodVisitor();
	}

	@Override
	public boolean isCancelable() {
		return getInput().getProgressMonitor().isSome();
	}

	@Override
	public boolean isCanceled() {
		Option<IProgressMonitor> monitor = getInput().getProgressMonitor();
		if (monitor.isSome())
			return monitor.unwrap().isCanceled();
		else
			return Thread.currentThread().isInterrupted();
	}

	@Override
	public void cancel() {
		Option<IProgressMonitor> monitor = getInput().getProgressMonitor();
		if (monitor.isSome())
			monitor.unwrap().setCanceled(true);
		// else do nothing
	}

	@Override
	public void reportUserProblem(String description, ASTNode node,
			Category category) {
		// arg: map from category to eclipse severity to crystal severity
		IAnalysisReporter.SEVERITY severity;
		switch (category.severity) {
		case IMarker.SEVERITY_ERROR:
			severity = IAnalysisReporter.SEVERITY.ERROR;
			break;
		case IMarker.SEVERITY_WARNING:
			severity = IAnalysisReporter.SEVERITY.WARNING;
			break;
		default:
			severity = IAnalysisReporter.SEVERITY.INFO;
			break;
		}
		reporter.reportUserProblem(description, node, getName(),
				severity);
	}

	@Override
	public RefType getLocalType(VariableDeclaration declaration) {
		List<ICrystalAnnotation> annos =
			getInput().getAnnoDB().getAnnosForVariable(declaration.resolveBinding());
		return getParamType(annos);
	}

	@Override
	public RefType getParamType(IMethodBinding binding, int paramIndex) {
		List<ICrystalAnnotation> annos =
			getInput().getAnnoDB().getSummaryForMethod(binding).getParameter(paramIndex);
		return getParamType(annos);
	}

	@Override
	public RefType getReceiverType(IMethodBinding binding) {
		List<ICrystalAnnotation> annos =
			getInput().getAnnoDB().getSummaryForMethod(binding).getReturn();
		return getParamType(annos);
	}

	@Override
	public RefType getVariableType(IVariableBinding binding) {
		List<ICrystalAnnotation> annos =
			getInput().getAnnoDB().getAnnosForVariable(binding);
		RefType result = getParamType(annos);
		if (result == null)
			return null;
		if (binding.isField() &&
				! result.getPerm().isSymmetric() && ! result.isBorrowed()) {
			try {
				// produce syntax error...
				ISourceReference ref = (ISourceReference) binding.getJavaElement();
				reportUserProblem(result.getPerm() + " cannot be consumed during unpacking: use permission that can be duplicated",
						binding.getJavaElement(),
						ref.getSourceRange().getOffset(),
						ref.getSourceRange().getLength(),
						Category.SYNTAX);
			} catch (JavaModelException e) {
				logger.log(Level.SEVERE, "Error retrieving source range", e);
			}
			return ObjectType.getInstance(result.getPerm(), true, false);
		}
		return result;
	}

	private RefType getParamType(List<ICrystalAnnotation> annos) {
		for (ICrystalAnnotation a : annos) {
			if (Excl.class.getName().equals(a.getName())) {
				return ObjectType.getInstance(PermKind.EXCL,
						(Boolean) a.getObject("borrowed"),
						(Boolean) a.getObject("released"),
						getPerms((Object[]) a.getObject("elems")));
			}
			if (Imm.class.getName().equals(a.getName())) {
				return ObjectType.getInstance(PermKind.IMM,
						(Boolean) a.getObject("borrowed"),
						(Boolean) a.getObject("released"),
						getPerms((Object[]) a.getObject("elems")));
			}
		}
		return null;
	}

	private PermKind[] getPerms(Object[] perms) {
		if (perms.length == 0)
			// avoid pointless array allocations in the very common default case
			return PermKind.EMPTY_PERM_KIND_ARRAY;
		PermKind[] result = new PermKind[perms.length];
		for (int i = 0; i < perms.length; ++i) {
			String perm = (String) perms[i];
			perm = perm.toUpperCase();
			result[i] = PermKind.valueOrNull(perm);
			if (result[i] == null) {
				// TODO report user problem
				logger.warning("Unknown permission kind: " + perms[i]);
			}
		}
		return result;
	}

	@Override
	public RefType getReturnType(IMethodBinding binding) {
		boolean released = false;
		AnnotationSummary summary =
			getInput().getAnnoDB().getSummaryForMethod(binding);

		// figure out if result is borrowed
		RefType receiverType = getParamType(summary.getReturn());
		if (receiverType != null && receiverType.isReleased()) {
			released = true;
		} else {
			int paramCount = summary.getParameterNames().length;
			for (int i = 0; i < paramCount; ++i) {
				RefType paramType = getParamType(summary.getParameter(i));
				if (paramType != null && paramType.isReleased()) {
					released = true;
					break;
				}
			}
		}

		// mark result as borrowed if any parameter is captured
		// TODO do not *require* capturing expression to be borrowed
		// technically the result doesn't have to be borrowed but
		// currently we wouldn't release permissions from the result expr,
		// leading to captured arguments not being released either

		if (binding.isConstructor())
			// make constructor always return exclusive permission
			return ObjectType.getInstance(PermKind.EXCL, released, false);

		List<ICrystalAnnotation> annos = summary.getReturn();
		for (ICrystalAnnotation a : annos) {
			if (ReturnExcl.class.getName().equals(a.getName())) {
				return ObjectType.getInstance(PermKind.EXCL, released, false,
						getPerms((Object[]) a.getObject("elems")));
			}
			if (ReturnImm.class.getName().equals(a.getName())) {
				return ObjectType.getInstance(PermKind.IMM, released, false,
						getPerms((Object[]) a.getObject("elems")));
			}
		}
		return null;
	}

	private void reportUserProblem(String description, IJavaElement element,
			int start, int length, Category category) {
		IResource resource = element.getResource();
		reportUserProblem(description,
				resource,
				start,
				start,
				category.severity);
	}

	private void reportUserProblem(String description, IResource resource,
			int start, int length, int sevMarker) {
		// Create Crystal marker (so it can be cleared as usual)
		try {
			IMarker marker = resource.createMarker(Crystal.MARKER_DEFAULT);
			marker.setAttribute(IMarker.CHAR_START, start);
			marker.setAttribute(IMarker.CHAR_END, start + length);
			marker.setAttribute(IMarker.MESSAGE, '[' + getName() + "] " + description);
			marker.setAttribute(IMarker.PRIORITY, IMarker.PRIORITY_NORMAL);
			marker.setAttribute(IMarker.SEVERITY, sevMarker);
			marker.setAttribute(Crystal.MARKER_ATTR_ANALYSIS, getName());
		} catch (CoreException ce) {
			logger.log(Level.SEVERE, "CoreException when creating marker", ce);
		}
	}

	@Override
	public Contract getContract(ClassInstanceCreation node) {
		return reg.getContract(node);
	}

	@Override
	public Contract getContract(ConstructorInvocation node) {
		return reg.getContract(node);
	}

	@Override
	public Contract getContract(MethodInvocation node) {
		return reg.getContract(node);
	}

	@Override
	public Contract getContract(SuperConstructorInvocation node) {
		return reg.getContract(node);
	}

	@Override
	public Contract getContract(SuperMethodInvocation node) {
		return reg.getContract(node);
	}

	@Override
	public Contract getContract(MethodDeclaration decl) {
		return reg.getContract(decl);
	}

	@Override
	public Boolean getNullChecksFlag(IBinding binding) {
		return getValueFlag(NullChecks.class, binding);
	}

	@Override
	public Boolean getBoundsChecksFlag(IBinding binding) {
		return getValueFlag(BoundsChecks.class, binding);
	}

	private Boolean getValueFlag(Class<? extends Annotation> annoClass, IBinding binding) {
		if (binding instanceof IMethodBinding) {
			return getValueFlag(annoClass,
					input.getAnnoDB().getSummaryForMethod((IMethodBinding) binding).getReturn());
		}
		if (binding instanceof ITypeBinding) {
			return getValueFlag(annoClass,
					input.getAnnoDB().getAnnosForType((ITypeBinding) binding));
		}
		throw new IllegalArgumentException("not type or method: " + binding);
	}

	private Boolean getValueFlag(Class<? extends Annotation> annoClass,
			List<ICrystalAnnotation> annos) {
		for (ICrystalAnnotation a : annos) {
			if (annoClass.getName().equals(a.getName()))
				return (Boolean) a.getObject("value");
		}
		return null;
	}

	public Formula encode(Expression e, Lookup lookup, Lookup preLookup) {
		if (reg instanceof JmlContractRegistry)
			return JmlExpressionEncoder.encode(e, lookup, preLookup);
		else
			return ExpressionEncoder.encode(e, lookup);
	}

	@Override
	public Collection<Expression> getLoopInvariant(Statement loopBody) {
		return reg.getLoopInvariant(loopBody);
	}

	@Override
	public Collection<Expression> getInvariants(ITypeBinding type) {
		return reg.getInvariants(type);
	}

	@Override
	public Collection<Expression> getInvariants(TypeDeclaration type) {
		return reg.getInvariants(type);
	}
}
